package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Screen {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Screen");
		 
		 //Clocks
		 tiosts.addClock("clockS");
		 
         // Variables
         TypedData coordinateS = new TypedData("coordinateS", Constants.TYPE_INTEGER);
         tiosts.addVariable(coordinateS);
         
         // Parameters
         TypedData position = new TypedData("position", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(position);
         
         // Input, output, and internal actions
         Action init = new Action("initS", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action simpleClick = new Action("simpleClick", Constants.ACTION_INPUT);
         simpleClick.addParameter(position.getName());
         tiosts.addAction(simpleClick);
         Action doubleClick = new Action("doubleClick", Constants.ACTION_INPUT);
         doubleClick.addParameter(position.getName());
         tiosts.addAction(doubleClick);
         Action printMenu = new Action("printMenu", Constants.ACTION_OUTPUT);
         printMenu.addParameter(position.getName());
         tiosts.addAction(printMenu);
         Action openApp = new Action("openApp", Constants.ACTION_OUTPUT);
         openApp.addParameter(position.getName());
         tiosts.addAction(openApp);
         
         // Locations
         Location start = new Location("StartS");
         tiosts.addLocation(start);
         Location s3 = new Location("S3");
         tiosts.addLocation(s3);
         Location s4 = new Location("S4");
         tiosts.addLocation(s4);   
         Location s5 = new Location("S5");
         tiosts.addLocation(s5);  
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("StartS", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S3");
         tiosts.createTransition("S3",  Constants.GUARD_TRUE, "clockS <= 3", simpleClick, "coordinateS := position", null, Constants.DEADLINE_LAZY, "S5");
         tiosts.createTransition("S5",  "coordinateS = position", Constants.GUARD_TRUE, printMenu, null, "clockS := 0", Constants.DEADLINE_LAZY, "S3");
         tiosts.createTransition("S3",  Constants.GUARD_TRUE, "clockS > 3", doubleClick, "coordinateS := position", null, Constants.DEADLINE_LAZY, "S4");
         tiosts.createTransition("S4",  "coordinateS = position", "clockS > 6", openApp, null, "clockS := 0", Constants.DEADLINE_LAZY, "S3");
         
         return tiosts;		 
	 }

}
